Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		lt(0,s(X))	→ true
2:		lt(s(X),0)	→ false
3:		lt(s(X),s(Y))	→ lt(X,Y)
4:		append(nil,Y)	→ Y
5:		append(add(N,X),Y)	→ add(N,append(X,Y))
6:		split(N,nil)	→ pair(nil,nil)
7:		split(N,add(M,Y))	→ f_1(split(N,Y),N,M,Y)
8:		f_1(pair(X,Z),N,M,Y)	→ f_2(lt(N,M),N,M,Y,X,Z)
9:		f_2(true,N,M,Y,X,Z)	→ pair(X,add(M,Z))
10:		f_2(false,N,M,Y,X,Z)	→ pair(add(M,X),Z)
11:		qsort(nil)	→ nil
12:		qsort(add(N,X))	→ f_3(split(N,X),N,X)
13:		f_3(pair(Y,Z),N,X)	→ append(qsort(Y),add(X,qsort(Z)))

There are 11 dependency pairs:


14:		LT(s(X),s(Y))	→ LT(X,Y)
15:		APPEND(add(N,X),Y)	→ APPEND(X,Y)
16:		SPLIT(N,add(M,Y))	→ F_1(split(N,Y),N,M,Y)
17:		SPLIT(N,add(M,Y))	→ SPLIT(N,Y)
18:		F_1(pair(X,Z),N,M,Y)	→ F_2(lt(N,M),N,M,Y,X,Z)
19:		F_1(pair(X,Z),N,M,Y)	→ LT(N,M)
20:		QSORT(add(N,X))	→ F_3(split(N,X),N,X)
21:		QSORT(add(N,X))	→ SPLIT(N,X)
22:		F_3(pair(Y,Z),N,X)	→ APPEND(qsort(Y),add(X,qsort(Z)))
23:		F_3(pair(Y,Z),N,X)	→ QSORT(Y)
24:		F_3(pair(Y,Z),N,X)	→ QSORT(Z)

The approximated dependency graph contains 4 SCCs: {15}, {14}, {17} and {20,23,24}.

Consider the SCC {15}. There are no usable rules. By taking the AF π with π(APPEND) = 1 and π(add) = [2] together with the lexicographic path order with empty precedence, rule 15 is strictly decreasing.

Consider the SCC {14}. There are no usable rules. By taking the AF π with π(LT) = 1 together with the lexicographic path order with empty precedence, rule 14 is strictly decreasing.

Consider the SCC {17}. There are no usable rules. By taking the AF π with π(SPLIT) = 2 and π(add) = [2] together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Consider the SCC {20,23,24}. The usable rules are {1-3,6-10}. The constraints could not be solved.

Tyrolean Termination Tool (47.20 seconds) --- May 4, 2006